$\forall$${\it es}$:ES, ${\it ff}$:FIFO, ${\it f2f+}$:F2F+{-}decls, $e$:E, ${\it sndr}$, ${\it rcvr}$:${\it ff}$.C.
\\[0ex]([$e$: ${\it sndr}$ $--$is\_req  $\rightarrow$ ${\it rcvr}$] $\Rightarrow$ (loc($e$) = ${\it sndr}$ $\in$ Id))
\\[0ex]\& ([$e$: ${\it rcvr}$ $--$is\_ack $\rightarrow$ ${\it sndr}$] $\Rightarrow$ (loc($e$) = ${\it rcvr}$ $\in$ Id))